(set-logic ALL)
(set-info :status unsat)
(declare-const x8 Bool)
(set-option :strings-exp true)
(declare-fun s () (Seq Int))
(declare-fun x () Int)
(declare-fun i () Int)
(declare-fun i@ () Int)
(assert (and (forall ((u Int)) (or (> 0 u) (>= u i) (distinct x (seq.nth s u))))
             (or (and x8 (not x8))
                 (and (= i@ (+ i 1))
                      (distinct x (seq.nth s i))
                      (exists ((u Int)) (and (<= 0 u)
                                             (< u i@)
                                             (= x (seq.nth s u))))
                 )
        )))
(check-sat)
